package ewu.expressions

import ewu._
import java.util.ArrayList
import scala.collection.mutable.ArrayBuffer

/**
 * Ein ExistsQuantor setzt sich aus einer freien Variable, einem Wertebereich 
 * und einer BoolExpression zusammen.
 * Die freie Variable durchlaeuft den Wertebereich solange, bis
 *   a) die BoolExpression fuer einen Wert gilt
 *   b) alle Werte fuer die BoolExpression false ergeben
 *   
 *   Ein ExistsQuantor ist eine BoolExpression die genau dann "true" ist, wenn
 *   die BoolExpression "booli" fuer mindestens einen Wert aus der ValueRange 
 *   "range" gilt.
 *   
 *   Ist der Wertebereich leer, so wird eine IllegalArgumentException geworfen
 *   Die to*Constructor-Methoden wurden nicht definiert.
 */

case class ExistsQuantor(variable: String, range: ValueRange, booli: BoolExpression) 
                                            extends Quantor(variable, range, booli) {
  override def toString: String = "(exists " + variable + " in " + range.toString + 
                                                          " : " + booli.toString + ")"

  def toAdaConstructor: String = ""

  def toAdaConstructor(t: Int): String = ""

  def toScalaConstructor: String = ""

  def toScalaConstructor(t: Int): String = ""

  def reduce: BoolExpression = booli.reduce

  def isTrue = false


  def evaluate(env: Environment): Option[Boolean] = {
//    if (range.isEmpty) {
//      throw new IllegalArgumentException("Range is empty")
//    }
//    else {
      var end: Boolean = false
      for (i <- range.toScalaRange) {
        if (end) {
          return Some(true)
        }
        else {
          env.addValue(variable, i)
          booli.evaluate(env) match {
            case Some(x)
            => end |= x
            case _ => throw new IllegalArgumentException("Expression not evaluable: " + booli.toString
              + "in environment: " + env.toString)
          }
        }

      }
      return Some(end)

//    }
  }
  
  def getVariables(a: ArrayBuffer[Name]) = {
    booli.getVariables(a);
  }
  
  override def replaceVariable(fromVar: Name, toVar: Expression) = {
    booli.replaceVariable(fromVar, toVar);
  }
  
 // Diese Funktion ersetzt diesen Quantor durch eine Funktion fuer die Check-Version.
 override def replaceQuantor(addfuncs: ArrayList[String], arrayvars: ArrayList[String]) 
    : BoolExpression = {
    var tvarsinbooli:ArrayBuffer[Name] = new ArrayBuffer()
    var varsinbooli:ArrayBuffer[Name] = new ArrayBuffer()
    var tpars = ""
    booli.getVariables(tvarsinbooli)
    for(i <- tvarsinbooli) {
      println(i + " : " + i.getClass)
      i match {
        case x:ArrayAtIndex =>
          if(!varsinbooli.contains(Name(x.name)) && !x.name.equals(variable)) {
            varsinbooli.append(Name(x.name))
          }
              
        case x:Name => 
          if(!varsinbooli.contains(Name(x.name)) && !x.name.equals(variable)) {
            varsinbooli.append(Name(x.name))
          }           
        case _ =>
      }
    }
    for(i <- varsinbooli) {
      if(arrayvars.contains(i.name))
        tpars += " " + i.name + ": IntArray;"
      else
        tpars += " " + i.name + ": Integer;"
    }
    var ta = new Array[Expression](2 + varsinbooli.length)
    ta(0) = range.fromE
    ta(1) = range.toE
    for(i <- 0 to varsinbooli.length-1) {
      ta(i+2) = varsinbooli(i)
    }
    
    var str = "   FUNCTION exists" + (addfuncs.size+1) + " (rangeS, rangeE: Integer;" + tpars
    str += ") RETURN Integer IS\n      " + variable + ": Integer = rangeS;\n      "
    str += "ret: Integer = 0;\n   BEGIN\n      WHILE " + variable + " <= rangeS LOOP\n"
    str += "         IF " + booli.replaceQuantor(addfuncs, arrayvars) + " THEN\n;"
    str += "            ret = 1;         END IF;\n"
    str += "         " + variable + " = " + variable + "+1;\n"
    str += "      END LOOP;\n      RETURN ret;\n   END exists" + (addfuncs.size+1) + ";"
    addfuncs.add(str)

    return new Equal(functionExpression("exists" + addfuncs.size, ta), new Number(1))
  }
}